CoinductiveBuiltinNatural.agda:9,21-22
ℕ !=< ∞ ℕ of type Set
when checking that the expression suc has type ℕ → ℕ
